<html>
<head><meta charset="utf-8"><title>extralogical reasoning · wg-traits · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/index.html">wg-traits</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/extralogical.20reasoning.html">extralogical reasoning</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="193279253"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/extralogical%20reasoning/near/193279253" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/extralogical.20reasoning.html#193279253">(Apr 08 2020 at 06:22)</a>:</h4>
<p>I need some guidance on chalk's stance on extralogical reasoning. For example, reasoning about struct fields is extralogical in the current implementation (WF program clauses do not consider fields, only WfSolver does). Where does the boundary lie?</p>



<a name="193452381"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/extralogical%20reasoning/near/193452381" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/extralogical.20reasoning.html#193452381">(Apr 09 2020 at 13:49)</a>:</h4>
<p>The reason Im interested is the Drop trait implementation: my current solution is to prohibit downstream implementations because from the Drop constraints we know that you can only implement Drop for your own structs. But I would really like inability to implement Drop in downstream crates to be deducted, not given.</p>



<a name="193618989"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/extralogical%20reasoning/near/193618989" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/extralogical.20reasoning.html#193618989">(Apr 10 2020 at 21:20)</a>:</h4>
<p>So, I don't have a ton of time to answer here just now, will try to elaborate more, but...</p>
<p>The way I see it, chalk has three 'main parts':</p>
<ul>
<li>The lower level logical engine, which interprets the clauses and goals it is given. </li>
<li>The translation from Rust syntax to those predicates. This layer, in effect, gives the "semantics" for the Rust trait system.</li>
<li>The definition of well-formedness rules for Rust items in terms of predicates.</li>
</ul>
<p>I think that it is the job of the "translation" and "well-formedness" layers to be "self-consistent", in some sense. Just expressing things in logical predicate form doesn't <em>by itself</em> mean that those predicates make any particular sense. </p>
<p>But it's totally valid to have some translation rules that only make sense because we know that the wf predicates will have to be proven. (Implied bounds totally rely on this concept, for example.)</p>



<a name="193619029"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/extralogical%20reasoning/near/193619029" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/extralogical.20reasoning.html#193619029">(Apr 10 2020 at 21:20)</a>:</h4>
<p>So I think what I'm saying is "yes that sort of extralogical reasoning is fine"</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>